Nuprl Lemma : p_equiv_wf
13,42
postcript
pdf
T
:Type,
A
,
B
:(
T
).
A
{
T
}
B
latex
Up
gen
algebra
1
Definitions of Statement
A
{
T
}
B
Definitions
P
&
Q
,
A
{
T
}
B
,
t
T
,
,
x
:
A
.
B
(
x
)
Lemmas
p
subset
wf
origin
T:Type, A, B:(T
). A 
{T} B 
T:Type, A, B:(T). A {T} B {T} B{T} B Tx:A. B(x)